Iof proof for Lemma add mono wrt lt rw:
a, b, n:
. {(a < b) 
((a+n) < (b+n))}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_lt`))
C.| 12,41 |
a, b, n:. {(a < b) ((a+n) < (b+n))}
by ((Unfold `guard` 0)
CollapseTHEN (Lemma `add_mono_wrt_lt`))
C.
| Definitions | |
| Lemmas |